--- Test case for 'https://github.com/Frege/frege/issues/336 #336'
{--
    Annotated constraint got lost when right hand side written in point free style
    didn't mention the higher rank constrained argument. That is, with
    
    > foo ∷ (∀a. Something a ⇒ a → a) → [b→b]
    
    the typechecker was happy. But note that the higher ranked function passed as argument to @foo@
    needs to get instantiated at some type (here "b") when passed to @pure@ (as @pure@ does not expect
    a higher ranked function). Such instantiation on constrained types implies that a 
    dictionary must be passed to satisfy the constraints (here @Something a@). And this
    dictionary can only come from the caller of @foo@, who knows what @b@ actually is.
    Hence, @Something b@ must occur in the type for @foo@.
    
    This type error was flagged only when the definition did mention the argument, for example:
    
    > foo f = pure f
    
    but not when it was written in the short form.
-}
module tests.comp.Issue336 where

foo :: (∀ a. Something a ⇒ a → a) → (∀ b. Something b ⇒ [b → b])
foo  = pure    

bar :: (∀ a. Something a ⇒ (∀ b. Something b ⇒ (∀ c. Something c ⇒ c → c) → b → b) → a → a)
bar f a = f identity a

-- for easier tracing, we dont use standard id which has a more complex type

identity x = x

class Something a

instance Something String

main = do
  println  ( head (foo identity)  "Ok" )    -- head [identity] "Ok"
  println  ( bar identity "Ok" )            -- identity identity "Ok"
